YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { half(0()) -> 0()
  , half(s(0())) -> 0()
  , half(s(s(x))) -> s(half(x))
  , bits(0()) -> 0()
  , bits(s(x)) -> s(bits(half(s(x)))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add following weak dependency pairs:

Strict DPs:
  { half^#(0()) -> c_1()
  , half^#(s(0())) -> c_2()
  , half^#(s(s(x))) -> c_3(half^#(x))
  , bits^#(0()) -> c_4()
  , bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { half^#(0()) -> c_1()
  , half^#(s(0())) -> c_2()
  , half^#(s(s(x))) -> c_3(half^#(x))
  , bits^#(0()) -> c_4()
  , bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
Strict Trs:
  { half(0()) -> 0()
  , half(s(0())) -> 0()
  , half(s(s(x))) -> s(half(x))
  , bits(0()) -> 0()
  , bits(s(x)) -> s(bits(half(s(x)))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { half(0()) -> 0()
    , half(s(0())) -> 0()
    , half(s(s(x))) -> s(half(x)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { half^#(0()) -> c_1()
  , half^#(s(0())) -> c_2()
  , half^#(s(s(x))) -> c_3(half^#(x))
  , bits^#(0()) -> c_4()
  , bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
Strict Trs:
  { half(0()) -> 0()
  , half(s(0())) -> 0()
  , half(s(s(x))) -> s(half(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(s) = {1}, Uargs(c_3) = {1}, Uargs(bits^#) = {1},
  Uargs(c_5) = {1}

TcT has computed following constructor-restricted matrix
interpretation.

           [0] = [2]
                 [0]
                    
    [half](x1) = [1 0] x1 + [1]
                 [0 0]      [1]
                               
       [s](x1) = [1 1] x1 + [2]
                 [0 0]      [0]
                               
  [half^#](x1) = [0]
                 [0]
                    
         [c_1] = [1]
                 [1]
                    
         [c_2] = [1]
                 [1]
                    
     [c_3](x1) = [1 0] x1 + [2]
                 [0 1]      [2]
                               
  [bits^#](x1) = [2 0] x1 + [0]
                 [0 0]      [0]
                               
         [c_4] = [1]
                 [0]
                    
     [c_5](x1) = [1 0] x1 + [1]
                 [0 1]      [2]

This order satisfies following ordering constraints


Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { half^#(0()) -> c_1()
  , half^#(s(0())) -> c_2()
  , half^#(s(s(x))) -> c_3(half^#(x))
  , bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
Weak DPs: { bits^#(0()) -> c_4() }
Weak Trs:
  { half(0()) -> 0()
  , half(s(0())) -> 0()
  , half(s(s(x))) -> s(half(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {1,2} by applications of
Pre({1,2}) = {3}. Here rules are labeled as follows:

  DPs:
    { 1: half^#(0()) -> c_1()
    , 2: half^#(s(0())) -> c_2()
    , 3: half^#(s(s(x))) -> c_3(half^#(x))
    , 4: bits^#(s(x)) -> c_5(bits^#(half(s(x))))
    , 5: bits^#(0()) -> c_4() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { half^#(s(s(x))) -> c_3(half^#(x))
  , bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
Weak DPs:
  { half^#(0()) -> c_1()
  , half^#(s(0())) -> c_2()
  , bits^#(0()) -> c_4() }
Weak Trs:
  { half(0()) -> 0()
  , half(s(0())) -> 0()
  , half(s(s(x))) -> s(half(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ half^#(0()) -> c_1()
, half^#(s(0())) -> c_2()
, bits^#(0()) -> c_4() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { half^#(s(s(x))) -> c_3(half^#(x))
  , bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
Weak Trs:
  { half(0()) -> 0()
  , half(s(0())) -> 0()
  , half(s(s(x))) -> s(half(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict
rules from (R) into the weak component:

Problem (R):
------------
  Strict DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
  Weak DPs: { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
  Weak Trs:
    { half(0()) -> 0()
    , half(s(0())) -> 0()
    , half(s(s(x))) -> s(half(x)) }
  StartTerms: basic terms
  Strategy: innermost

Problem (S):
------------
  Strict DPs: { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
  Weak DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
  Weak Trs:
    { half(0()) -> 0()
    , half(s(0())) -> 0()
    , half(s(s(x))) -> s(half(x)) }
  StartTerms: basic terms
  Strategy: innermost

Overall, the transformation results in the following sub-problem(s):

Generated new problems:
-----------------------
R) Strict DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
   Weak DPs: { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   Weak Trs:
     { half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x)) }
   StartTerms: basic terms
   Strategy: innermost
   
   This problem was proven YES(O(1),O(n^1)).

S) Strict DPs: { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   Weak DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
   Weak Trs:
     { half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x)) }
   StartTerms: basic terms
   Strategy: innermost
   
   This problem was proven YES(O(1),O(n^1)).


Proofs for generated problems:
------------------------------
R) We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
   Weak DPs: { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   Weak Trs:
     { half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
   Weak Trs:
     { half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   No rule is usable, rules are removed from the input problem.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   We use the processor 'matrix interpretation of dimension 1' to
   orient following rules strictly.
   
   DPs:
     { 1: half^#(s(s(x))) -> c_3(half^#(x)) }
   
   Sub-proof:
   ----------
     The following argument positions are usable:
       Uargs(c_3) = {1}
     
     TcT has computed following constructor-based matrix interpretation
     satisfying not(EDA).
     
                [0] = [0]
                         
         [half](x1) = [1] x1 + [0]
                                  
            [s](x1) = [1] x1 + [2]
                                  
       [half^#](x1) = [1] x1 + [0]
                                  
          [c_3](x1) = [1] x1 + [0]
                                  
       [bits^#](x1) = [1] x1 + [0]
                                  
          [c_5](x1) = [1] x1 + [0]
     
     This order satisfies following ordering constraints
     
       [half^#(s(s(x)))] = [1] x + [4]     
                         > [1] x + [0]     
                         = [c_3(half^#(x))]
                                           
   
   The strictly oriented rules are moved into the corresponding weak
   component(s).
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Weak DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { half^#(s(s(x))) -> c_3(half^#(x)) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Rules: Empty
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   Empty rules are trivially bounded

S) We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs: { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   Weak DPs: { half^#(s(s(x))) -> c_3(half^#(x)) }
   Weak Trs:
     { half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { half^#(s(s(x))) -> c_3(half^#(x)) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs: { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   Weak Trs:
     { half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   We use the processor 'matrix interpretation of dimension 2' to
   orient following rules strictly.
   
   DPs:
     { 1: bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   Trs: { half(s(0())) -> 0() }
   
   Sub-proof:
   ----------
     The following argument positions are usable:
       Uargs(c_5) = {1}
     
     TcT has computed following constructor-based matrix interpretation
     satisfying not(EDA) and not(IDA(1)).
     
                [0] = [0]
                      [0]
                         
         [half](x1) = [0 1] x1 + [0]
                      [0 1]      [0]
                                    
            [s](x1) = [0 1] x1 + [2]
                      [0 1]      [1]
                                    
       [half^#](x1) = [1 1] x1 + [0]
                      [0 0]      [0]
                                    
          [c_3](x1) = [1 1] x1 + [0]
                      [0 0]      [0]
                                    
       [bits^#](x1) = [1 2] x1 + [0]
                      [0 0]      [0]
                                    
          [c_5](x1) = [1 0] x1 + [0]
                      [0 0]      [0]
     
     This order satisfies following ordering constraints
     
           [half(0())] =  [0]                      
                          [0]                      
                       >= [0]                      
                          [0]                      
                       =  [0()]                    
                                                   
        [half(s(0()))] =  [1]                      
                          [1]                      
                       >  [0]                      
                          [0]                      
                       =  [0()]                    
                                                   
       [half(s(s(x)))] =  [0 1] x + [2]            
                          [0 1]     [2]            
                       >= [0 1] x + [2]            
                          [0 1]     [1]            
                       =  [s(half(x))]             
                                                   
        [bits^#(s(x))] =  [0 3] x + [4]            
                          [0 0]     [0]            
                       >  [0 3] x + [3]            
                          [0 0]     [0]            
                       =  [c_5(bits^#(half(s(x))))]
                                                   
   
   The strictly oriented rules are moved into the corresponding weak
   component(s).
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Weak DPs: { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   Weak Trs:
     { half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { bits^#(s(x)) -> c_5(bits^#(half(s(x)))) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Weak Trs:
     { half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   No rule is usable, rules are removed from the input problem.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Rules: Empty
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   Empty rules are trivially bounded


Hurray, we answered YES(O(1),O(n^1))